ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), x:Id, T:Type, ks:(Knd List),
a:((k:{k:Knd| (k  ks)} decl-state(ds)ma-valtype(da; k)T)), snd:msg-spec(ds; da), i:Id.
normal-type{i:l}
normal-type(T)
 normal-ds{i:l}
 normal-ds(ds)
 normal-da{i:l}
 normal-da(da)
 l_all(ks; Knd; k.((isrcv(k))  (i = destination(lnk(k))  Id)))
 msg-spec-loc-decl(snd; i; da)
 l_all(ks; Knd; k.(fpf-dom(Kind-deq; k; da)))
 ((fpf-dom(id-deq; x; ds)))
 R-realizes{i:l}
 R-realizes(ecl-machine3(ds; da; x; T; ks; a; snd);
 R-realizes(es.l_all(remove-repeats(idlnk-deq; msg-spec-links(snd));
 R-realizes(es.l_all(IdLnk;
 R-realizes(es.l_all(l.(es-decls(es;source(l);fpf-join(id-deq; ds; fpf-single(x; T));da)
 R-realizes(es.l_all( with decls fpf-join(id-deq; ds; fpf-single(x; T)) 
 R-realizes(es.l_all( with decls da
 R-realizes(es.l_all( sends on l from e 
 R-realizes(es.l_all( include if deq-member(Kind-deq; es-kind(es; e); ks)
 R-realizes(es.l_all( include then tagged-list-messages(es-state-when(es; e);
 R-realizes(es.l_all( include then tagged-list-messages(es-val(es; e);
 R-realizes(es.l_all( include then tagged-list-messages((ecl-m3(a; snd; x; l)(es-kind(es; e))))
 R-realizes(es.l_all( include else []
 R-realizes(es.l_all( include fi  
 R-realizes(es.l_all( and only these for tags in ecl-tags(l; snd)))) 

latex

Definitions

t.1, top, guard(T), sq_type(T), P  Q, P  Q, ff, subtype(S; T), tt, P  Q, A  B, x,y. t(x;y), False, A c B, x:A. B(x), x. t(x), t  T, P  Q, prop{i:l}, if b then t else f fi , IdLnk, ecl-machine3(ds; da; x; T; ks; a; snd), A, l_all(L; T; x.P(x)), P  Q, msg-spec(ds; da), decl-state(ds), (x  l), fpf(A; a.B(a)), x:A. B(x), msg-spec-loc(snd; i), decidable(P), msg-item(ds; da; k; l), msg-spec-loc-decl(snd; i; da), fpf-cap(f; eq; x; z), Unit, x(s1,s2), x(s), , , , ma-valtype(da; k)

Lemmas

R-lnk-tags-compat2, R-compat wf, decidable equal IdLnk, msg-spec-loc-decl-implies, member-remove-repeats, nil member, decidable assert, fpf-ap wf, member map, bool sq, fpf wf, product-deq wf, bool cases, member-ecl-tags, no repeats-ecl-tags, normal-ds-single, fpf-single wf, normal-ds-join, R-lnk-tags-rule, ma-valtype wf, decl-state wf, nat wf, pi2 wf, pi1 wf, msg-item wf, IdLnk wf, normal-type wf, normal-ds wf, normal-da wf, lnk wf, ldst wf, isrcv wf, l all wf2, msg-spec-loc-decl wf, Kind-deq wf, fpf-trivial-subtype-top, id-deq wf, Id wf, fpf-dom wf, es-tag wf, es-lnk wf, not functionality wrt iff, assert of bnot, eqff to assert, not wf, bnot wf, es-isrcv wf, es-decls-iff, es-vartype wf, es-state-subtype, es-state-when wf, rcv wf, Knd wf, top wf, fpf-cap wf, tagged-list-messages wf, assert-deq-member, eqtt to assert, assert wf, iff transitivity, bool wf, es-sends-iff wf, select wf, length wf1, ecl-m3 wf, ecl-tags wf, fpf-single wf3, fpf-join wf, R-lnk-tags wf, l member wf, msg-spec-links wf, idlnk-deq wf, remove-repeats wf, R-all-rule